Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	active(nats)	→ mark(adx(zeros))
2:	active(zeros)	→ mark(cons(0,zeros))
3:	active(incr(cons(X,Y)))	→ mark(cons(s(X),incr(Y)))
4:	active(adx(cons(X,Y)))	→ mark(incr(cons(X,adx(Y))))
5:	active(hd(cons(X,Y)))	→ mark(X)
6:	active(tl(cons(X,Y)))	→ mark(Y)
7:	active(adx(X))	→ adx(active(X))
8:	active(incr(X))	→ incr(active(X))
9:	active(hd(X))	→ hd(active(X))
10:	active(tl(X))	→ tl(active(X))
11:	adx(mark(X))	→ mark(adx(X))
12:	incr(mark(X))	→ mark(incr(X))
13:	hd(mark(X))	→ mark(hd(X))
14:	tl(mark(X))	→ mark(tl(X))
15:	proper(nats)	→ ok(nats)
16:	proper(adx(X))	→ adx(proper(X))
17:	proper(zeros)	→ ok(zeros)
18:	proper(cons(X1,X2))	→ cons(proper(X1),proper(X2))
19:	proper(0)	→ ok(0)
20:	proper(incr(X))	→ incr(proper(X))
21:	proper(s(X))	→ s(proper(X))
22:	proper(hd(X))	→ hd(proper(X))
23:	proper(tl(X))	→ tl(proper(X))
24:	adx(ok(X))	→ ok(adx(X))
25:	cons(ok(X1),ok(X2))	→ ok(cons(X1,X2))
26:	incr(ok(X))	→ ok(incr(X))
27:	s(ok(X))	→ ok(s(X))
28:	hd(ok(X))	→ ok(hd(X))
29:	tl(ok(X))	→ ok(tl(X))
30:	top(mark(X))	→ top(proper(X))
31:	top(ok(X))	→ top(active(X))

There are 43 dependency pairs:


32:	ACTIVE(nats)	→ ADX(zeros)
33:	ACTIVE(zeros)	→ CONS(0,zeros)
34:	ACTIVE(incr(cons(X,Y)))	→ CONS(s(X),incr(Y))
35:	ACTIVE(incr(cons(X,Y)))	→ S(X)
36:	ACTIVE(incr(cons(X,Y)))	→ INCR(Y)
37:	ACTIVE(adx(cons(X,Y)))	→ INCR(cons(X,adx(Y)))
38:	ACTIVE(adx(cons(X,Y)))	→ CONS(X,adx(Y))
39:	ACTIVE(adx(cons(X,Y)))	→ ADX(Y)
40:	ACTIVE(adx(X))	→ ADX(active(X))
41:	ACTIVE(adx(X))	→ ACTIVE(X)
42:	ACTIVE(incr(X))	→ INCR(active(X))
43:	ACTIVE(incr(X))	→ ACTIVE(X)
44:	ACTIVE(hd(X))	→ HD(active(X))
45:	ACTIVE(hd(X))	→ ACTIVE(X)
46:	ACTIVE(tl(X))	→ TL(active(X))
47:	ACTIVE(tl(X))	→ ACTIVE(X)
48:	ADX(mark(X))	→ ADX(X)
49:	INCR(mark(X))	→ INCR(X)
50:	HD(mark(X))	→ HD(X)
51:	TL(mark(X))	→ TL(X)
52:	PROPER(adx(X))	→ ADX(proper(X))
53:	PROPER(adx(X))	→ PROPER(X)
54:	PROPER(cons(X1,X2))	→ CONS(proper(X1),proper(X2))
55:	PROPER(cons(X1,X2))	→ PROPER(X1)
56:	PROPER(cons(X1,X2))	→ PROPER(X2)
57:	PROPER(incr(X))	→ INCR(proper(X))
58:	PROPER(incr(X))	→ PROPER(X)
59:	PROPER(s(X))	→ S(proper(X))
60:	PROPER(s(X))	→ PROPER(X)
61:	PROPER(hd(X))	→ HD(proper(X))
62:	PROPER(hd(X))	→ PROPER(X)
63:	PROPER(tl(X))	→ TL(proper(X))
64:	PROPER(tl(X))	→ PROPER(X)
65:	ADX(ok(X))	→ ADX(X)
66:	CONS(ok(X1),ok(X2))	→ CONS(X1,X2)
67:	INCR(ok(X))	→ INCR(X)
68:	S(ok(X))	→ S(X)
69:	HD(ok(X))	→ HD(X)
70:	TL(ok(X))	→ TL(X)
71:	TOP(mark(X))	→ TOP(proper(X))
72:	TOP(mark(X))	→ PROPER(X)
73:	TOP(ok(X))	→ TOP(active(X))
74:	TOP(ok(X))	→ ACTIVE(X)

The approximated dependency graph contains 9 SCCs: {48,65}, {66}, {50,69}, {49,67}, {68}, {51,70}, {53,55,56,58,60,62,64}, {41,43,45,47} and {71,73}.

Consider the SCC {48,65}. There are no usable rules. By taking the AF π with π(ADX) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 48 is weakly decreasing and rule 65 is strictly decreasing. There is one new SCC.
- Consider the SCC {48}. By taking the AF π with π(ADX) = 1 together with the lexicographic path order with empty precedence, rule 48 is strictly decreasing.

Consider the SCC {66}. There are no usable rules. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 66 is strictly decreasing.

Consider the SCC {50,69}. There are no usable rules. By taking the AF π with π(HD) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 50 is weakly decreasing and rule 69 is strictly decreasing. There is one new SCC.
- Consider the SCC {50}. By taking the AF π with π(HD) = 1 together with the lexicographic path order with empty precedence, rule 50 is strictly decreasing.

Consider the SCC {49,67}. There are no usable rules. By taking the AF π with π(INCR) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 49 is weakly decreasing and rule 67 is strictly decreasing. There is one new SCC.
- Consider the SCC {49}. By taking the AF π with π(INCR) = 1 together with the lexicographic path order with empty precedence, rule 49 is strictly decreasing.

Consider the SCC {68}. There are no usable rules. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 68 is strictly decreasing.

Consider the SCC {51,70}. There are no usable rules. By taking the AF π with π(mark) = π(TL) = 1 together with the lexicographic path order with empty precedence, rule 51 is weakly decreasing and rule 70 is strictly decreasing. There is one new SCC.
- Consider the SCC {51}. By taking the AF π with π(TL) = 1 together with the lexicographic path order with empty precedence, rule 51 is strictly decreasing.

Consider the SCC {53,55,56,58,60,62,64}. There are no usable rules. By taking the AF π with π(adx) = π(hd) = π(incr) = π(PROPER) = π(s) = π(tl) = 1 together with the lexicographic path order with empty precedence, the rules in {53,58,60,62,64} are weakly decreasing and the rules in {55,56} are strictly decreasing. There is one new SCC.
- Consider the SCC {53,58,60,62,64}. By taking the AF π with π(adx) = π(hd) = π(incr) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {53,58,60,62} are weakly decreasing and rule 64 is strictly decreasing. There is one new SCC.
  - Consider the SCC {53,58,60,62}. By taking the AF π with π(adx) = π(hd) = π(incr) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {53,58,62} are weakly decreasing and rule 60 is strictly decreasing. There is one new SCC.
    - Consider the SCC {53,58,62}. By taking the AF π with π(adx) = π(hd) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {53,62} are weakly decreasing and rule 58 is strictly decreasing. There is one new SCC.
      - Consider the SCC {53,62}. By taking the AF π with π(adx) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 53 is weakly decreasing and rule 62 is strictly decreasing. There is one new SCC.
        
        Consider the SCC {53}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 53 is strictly decreasing.

Consider the SCC {41,43,45,47}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(adx) = π(hd) = π(incr) = 1 together with the lexicographic path order with empty precedence, the rules in {41,43,45} are weakly decreasing and rule 47 is strictly decreasing. There is one new SCC.
- Consider the SCC {41,43,45}. By taking the AF π with π(ACTIVE) = π(adx) = π(hd) = 1 together with the lexicographic path order with empty precedence, the rules in {41,45} are weakly decreasing and rule 43 is strictly decreasing. There is one new SCC.
  - Consider the SCC {41,45}. By taking the AF π with π(ACTIVE) = π(adx) = 1 together with the lexicographic path order with empty precedence, rule 41 is weakly decreasing and rule 45 is strictly decreasing. There is one new SCC.
    - Consider the SCC {41}. By taking the AF π with π(ACTIVE) = 1 together with the lexicographic path order with empty precedence, rule 41 is strictly decreasing.

Consider the SCC {71,73}. The usable rules are {1-29}. The constraints could not be solved.

Tyrolean Termination Tool (176.78 seconds) --- May 3, 2006